Formal verification techniques verify whether the design intent of a specification for a circuit design is preserved in a particular implementation of the circuit. The design intent for a circuit design is specified using various assertions. The formal verification techniques verify whether these assertions hold true. Conventional formal verification techniques do not consider certain types of input specification, for example, low power specification. Low power design may be specified using unified power format (UPF).
In low power design, each portion of the circuit belongs to a power domain. Certain power domains can switch off during certain modes of the circuit. For example, certain portions of a circuit are on during normal operations of a device but are off in a low power mode. If a portion of a circuit is off during a mode, the outputs of that portion of the circuit carry an undefined signal. If this undefined signal reaches as input to other portions of the circuit, the signals propagating through these portions of the circuit also become undefined. As a result, power on/off combinations based on various low power modes can cause connectivity analysis results to be invalid. Conventional formal verification techniques do not take into account the low power design specification. Therefore, the results of formal verification of the circuit design may be erroneous. As a result, conventional formal verification techniques used in design of circuits that include low power specification are inadequate and may not provide accurate results.